|
|
Učení se automatů pro rychlou detekci anomálií v síťovém provozu
Hošták, Viliam Samuel ; Matoušek, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Táto práca sa zaoberá rýchlou detekciou sieťových anomálií na základe učenia automatov. Popisuje a porovnáva niekoľko vybraných algoritmov učenia automatov, vrátane ich aplikácie na učenie sieťových charakteristík. Pre takto naučené automaty je navrhnutých niekoľko metód detekcie sieťových anomálií, ktoré umožňujú odhaliť tak sekvenčné, ako aj štatistické anomálie v rámci komunikácie. Za týmto účelom využívajú mechanizmy samotných automatov, ich transformáciu, či štatistickú analýzu. Navrhované metódy detekcie boli implementované a vyhodnotené na prevádzke protokolu IEC 60870-5-104 používaného v industriálnych kontrolných systémoch.
|
|
|
Srovnání rychlosti moderních systémů pro vyhledávání regulárních výrazů
Trávníček, Jan ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Tato bakalářská práce popisuje způsob srovnání rychlosti moderních nástrojů pro vyhledávání regulárních výrazů. Pro srovnání rychlosti jednotlivých nástrojů je použita množina regulárních výrazů z IDS systému Snort, kde jsou zadány v PCRE notaci. Tyto regulární výrazy jsou vyhodnocovány různými nástroji a získané výsledky jsou porovnávány mezi sebou. V této práci je také řešen matematický a praktický pohled na pojem regulární výraz a převod regulárních výrazů jazyka Perl do notace regulárních výrazů POSIX.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Efficient Algorithms for Counting Automata
Mikšaník, David ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Counting automata (CAs) are classical finite automata extended with bounded counters. They still denote the class of regular languages but in a more compact way than finite automata. Since CAs are a recent model, there is a gap in the knowledge of efficient algorithms implementing various operations on the CAs. In this thesis, we mainly focus on an existing subclass of CAs called monadic counting automata (MCAs), i.e., CAs with counting loops on character classes, which are common in practice (e.g., detection of packets in network traffic, log analysis). For this subclass, we efficiently solve the emptiness and inclusion problems. Moreover, we provide two extensions of the class of MCAs (but not beyond the class of CAs) and efficiently solve the emptiness problem for them. MCAs naturally arise from regular expressions that are extended by the counting operator limited only to character classes. Thus our algorithm solving the inclusion problem of MCAs can be used in a new method for solving the inclusion problem of such regular expressions. We experimentally evaluated this method on regular expressions from a wide range of applications and compared it with the naive method. The experiments show that the method using our algorithm is less prone the explode. It also outperforms the naive method if the regular expressions contain counting operators with large bounds. As expected, for the easy cases, the naive method is still faster than the method based on our algorithm.
|
|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
Kontextem řízený lexikální analyzátor
Hatina, Peter ; Koutný, Jiří (oponent) ; Čermák, Martin (vedoucí práce)
Tato práce se věnuje základním principům lexikální analýzy a způsobu kontextového rozpoznání typu lexému v závislosti na jeho pozici ve zdrojovém souboru. V práci bude popsán princip lexikální analýzy, postup tvorby lexikálního analyzátoru a možné řešení kontextového rozlišení lexémů, založené na automatovém systému. Lexikální analyzátor je rozšířen o vlastnost rozpoznávat tokeny v blocích kódu dalších jazyků.
|
|
|
Efektivní funkcionální knihovna pro konečné automaty
Říha, Jakub ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
Konečné automaty jsou důležitou matematickou abstrakcí. Ve formální verifikaci se konečné automaty používají ke stručné reprezentaci regulárních jazyků. V této souvislosti se používají operace nad konečnými automaty, jako je testování jazykové univerzality a inkluze. Naivní přístup k implementaci těchto operací vede k explicitní determinizaci konečného automatu, což může být nakladné a nežádoucí. Nicméně existuje pokročilejší metoda k vykonávání těchto operací nazývaná Antichains algoritmus, která se vyhýbá explicitní determinizaci. Tato práce se zabývá efektivní implementací operací nad konečnými automaty v Haskellu a také porovnává několik implementačních variant. Získané výsledky jsou poté porovnány s knihovnou VATA, což je imperativní implementace knihovny pro práci nad konečnými automaty.
|
|
|
Implementace obecného zpětného assembleru
Přikryl, Zdeněk ; Masařík, Karel (oponent) ; Lukáš, Roman (vedoucí práce)
Tato práce popisuje proces vytváření disassembleru pro nově navrhované procesory. Kritériem při vytváření je jeho automatické vygenerování. Instrukční sada pro procesor je modelována pomocí specializovaného jazyka ISAC, který obsluhuje prostředky pro popis této instrukční sady, jako je například formát instrukce v jazyku symbolických instrukcí, binární zápis instrukce a chování instrukce. Vnitřním modelem je párový konečný automat, který formálně popíše vztah mezi textovou reprezentací instrukce a binárním kódováním instrukce. Z tohoto vnitřního modelu je generován kód překladače - disassembleru. Ten na vstupu přijímá program ve strojovém kódu a generuje ekvivalentní program v jazyce symbolických instrukcí.
|
|
|
Nové struktury a operace v matematické informatice
Bureš, Richard ; Krčmář, Radim (oponent) ; Meduna, Alexandr (vedoucí práce)
Cílem této práce je podívat se na některé známé a na některé v této práci vytvořené operace a na jejich vlastnosti nad především regulárními, ale i bezkontextovými jazyky. Dále si zde ukážeme, jak je možné takové operace provádět nad konečnými a zásobníkovými automaty a nakonec také jak je možné tyto automaty a operace nad nimi implementovat.
|
host ::
RSS.